Section: New Results

Safety

Participants : Patrick Cousot, Radhia Cousot.

The abstract interpretation design principle has been applied to the design of new forward and backward proof, verification and analysis methods for safety [17] . The safety collecting semantics defining the strongest safety property of programs is first expressed in a constructive fixpoint form. Safety proof and checking/verification methods then immediately follow by fixpoint induction. Static analysis of abstract safety properties such as invariance are constructively designed by fixpoint abstraction (or approximation) to (automatically) infer safety properties.